(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 5))
(let ((e4 1))
(let ((e5 (- v2)))
(let ((e6 (/ e3 e4)))
(let ((e7 (- v2 v1)))
(let ((e8 (* (- e3) v1)))
(let ((e9 (+ v2 e7)))
(let ((e10 (- v1)))
(let ((e11 (+ v2 v0)))
(let ((e12 (<= e9 e7)))
(let ((e13 (distinct e9 e8)))
(let ((e14 (distinct v0 e10)))
(let ((e15 (= e8 e11)))
(let ((e16 (distinct e9 v2)))
(let ((e17 (distinct e10 e7)))
(let ((e18 (< e9 e6)))
(let ((e19 (< v0 e6)))
(let ((e20 (distinct e5 e5)))
(let ((e21 (>= v2 e11)))
(let ((e22 (< e10 v0)))
(let ((e23 (< e6 e10)))
(let ((e24 (> e10 v2)))
(let ((e25 (< v2 v0)))
(let ((e26 (> e6 e8)))
(let ((e27 (< e6 e5)))
(let ((e28 (>= v0 v1)))
(let ((e29 (>= e11 e9)))
(let ((e30 (= v2 e5)))
(let ((e31 (= e11 e6)))
(let ((e32 (<= e11 e11)))
(let ((e33 (>= e10 e7)))
(let ((e34 (distinct e11 v0)))
(let ((e35 (>= e11 v0)))
(let ((e36 (distinct v2 e9)))
(let ((e37 (= e6 v1)))
(let ((e38 (distinct e11 v1)))
(let ((e39 (< e7 e7)))
(let ((e40 (<= e9 e10)))
(let ((e41 (distinct v2 e10)))
(let ((e42 (distinct e8 v0)))
(let ((e43 (or e16 e36)))
(let ((e44 (xor e20 e28)))
(let ((e45 (or e13 e27)))
(let ((e46 (or e30 e15)))
(let ((e47 (and e12 e26)))
(let ((e48 (xor e44 e29)))
(let ((e49 (= e39 e19)))
(let ((e50 (and e43 e17)))
(let ((e51 (not e22)))
(let ((e52 (and e42 e42)))
(let ((e53 (ite e32 e14 e21)))
(let ((e54 (xor e41 e52)))
(let ((e55 (=> e34 e46)))
(let ((e56 (not e33)))
(let ((e57 (= e37 e38)))
(let ((e58 (ite e51 e18 e50)))
(let ((e59 (ite e35 e24 e48)))
(let ((e60 (or e49 e57)))
(let ((e61 (ite e56 e23 e54)))
(let ((e62 (xor e40 e40)))
(let ((e63 (and e25 e59)))
(let ((e64 (and e61 e61)))
(let ((e65 (or e58 e31)))
(let ((e66 (= e63 e45)))
(let ((e67 (and e53 e53)))
(let ((e68 (= e47 e62)))
(let ((e69 (or e55 e66)))
(let ((e70 (or e67 e68)))
(let ((e71 (or e60 e70)))
(let ((e72 (or e64 e65)))
(let ((e73 (and e69 e69)))
(let ((e74 (or e71 e72)))
(let ((e75 (xor e73 e74)))
e75
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
